15 test programs exercising dependent function types and lambdas:
- Positive: pi_basic, pi_lambda_arg, pi_polymorphic_id, pi_const,
  pi_compose, pi_polycompose, pi_nested, pi_dependent_ret,
  pi_repeat, pi_staging_hof
- Error: pi_apply_non_fn, pi_lambda_type_mismatch, pi_lambda_in_object,
  pi_arity_mismatch, pi_lambda_missing_annotation

Snapshot outputs will be generated once the implementation lands.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

- Fix lambda param type parsing: use parse_atom_owned() instead of
  parse_expr() so the closing | is not consumed as BitOr
- Support postfix call syntax expr(args) in the expression parser
- Unify FunName::Name(Name) into FunName::Term(&Term) so named calls
  are a special case of expression calls
- Fix wildcard_enum_match_arm clippy lints in checker and pretty printer
- Fix match_same_arms for Pi/Lift/U all inhabiting TYPE
- Fix MetaVal variant name mismatches in eval (VLit/VCode/VTy/VClosure
  → Lit/Code/Ty/Closure)
- Update and add snapshots for pi_compose, pi_const, pi_lambda_arg,
  pi_repeat, pi_staging_hof, and others

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Introduce a local `eval_bump` arena for temporary allocations during
staging (synthetic Lam wrappers for global closures).  `Term` is
covariant, so `'core` data coerces to the shorter `'eval` lifetime.

- `MetaVal<'out, 'eval>` / `Binding` / `Env`: two lifetimes; `Closure.body`
  is `&'eval Term<'eval>`, covering both input terms and eval-arena allocs
- All internal eval functions gain `eval_arena: &'eval Bump`
- `unstage_program<'out, 'core>`: two lifetimes restored; `core_program`
  may be dropped once the function returns
- `cli/main.rs`: restore separate `core_arena` / `out_arena`

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Replace the two separate application nodes with a single `App { func,
args }` where `func` is any `Term` — `Term::Prim(p)` for primitives,
`Term::Global(name)` for top-level calls, etc. Empty args now
distinguishes `f()` from a bare `f` reference. No implicit currying in
the core IR; the typechecker checks arity explicitly.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

The lint is too aggressive when wildcards are used for non-exhaustive
dispatch (e.g. inner match on App callee kind).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Replace single-param Pi/Lam with a slice of (name, type) pairs,
enabling proper arity checking at the call site and allowing empty
parameter lists (thunks: `fn() -> T`).

- core: Pi and Lam now carry `params: &[(&str, &Term)]`
- checker: upfront arity check in App; dependent subst of earlier
  args into later param types; Lam type_of builds variadic Pi
- eval: zero-param Lam produces a Closure; zero-arg App calls
  force_thunk (returns already-evaluated values as-is)
- subst, alpha_eq, pretty: updated for variadic params
- test: add pi_lambda_empty_params showing thunk round-trip

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Pi now carries a `phase: Phase` field, making meta-level and object-level
function types distinct in the core IR. This allows the globals table to
store `&Term` (always a Pi) instead of `FunSig`, unifying type lookup for
globals and locals — both are now `&Term` lookups.

- core: add `phase` to `Pi`; remove `FunSig`; `Function` stores `ty: &Term`
  (always a Pi) with a `pi()` convenience method
- checker: globals table is now `HashMap<Name, &Term>`; `type_of(Global)`
  returns the stored Pi directly with no conversion; phase check for calls
  reads `pi.phase` instead of `sig.phase`; elaborate_sig returns `&Term`
- eval: `GlobalDef` stores `ty: &Term`; staging constructs a Pi term for
  the output Function
- subst, alpha_eq, pretty: propagate/compare/display `pi.phase`
- tests: update helpers and inline FunSig literals to Pi term construction

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Switch Term::Var from Lvl (absolute) to Ix (De Bruijn index, 0 = innermost).
Add core/value.rs with a semantic value domain (Value, VLam, VPi, Closure)
and the three NbE functions eval/inst/quote. Delete the broken subst.rs.

The checker now maintains an NbE environment (env + types as Values, lvl)
and uses eval + Pi-closure application instead of syntactic substitution when
checking dependent function call arguments. This fixes the variable-capture bug
where substituting a replacement containing binders could produce stale indices.

The staging evaluator is updated for Ix-based variable lookup and gains
index-shift logic for Code values: a Code { term, depth } now records the
output depth at creation time, and shift_free_ix adjusts free Ix values when
a code value is spliced into a deeper context. Without this fix the accumulator
variable in power_acc/power_acc_1 was wrongly resolved to the innermost binding.

Also adds stage snapshots for let_type and pi_nested_polymorphic (the latter
now type-checks correctly: apply_twice(u64, inc, 0) = 2).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- Add memory management notes to CLAUDE.md for NbE/closure patterns
- Create docs/bs/nbe_and_debruijn.md: comprehensive guide to NbE, De Bruijn
  representation (Ix vs Lvl), and free variable index shifting for staging
- Update docs/bs/pi_types.md to reflect recent changes:
  - Replace substitution with NbE in type checking
  - Document variadic Pi/Lam parameters
  - Remove outdated FunSig and single-param references
  - Clarify distinction between checker NbE and staging evaluator
- Enhance 2ltt skill with implementation architecture:
  - Add sections 7-10: NbE design, staging evaluator, De Bruijn shifts,
    reference implementations, glossary
  - Link to elaboration-zoo and local documentation

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

- Create docs/README.md: index of language design and implementation docs
- Update docs/bs/README.md: add new nbe_and_debruijn.md and clarify pi_types.md
- Update CLAUDE.md: add Documentation section with guidance to keep indices
  up to date when adding new files

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

- Update all test assertions to use val_type_of directly instead of the
  type_of wrapper, working directly with semantic Value domain
- Remove type_of public method from Ctx (was only quoting val_type_of)
- Update all test pattern matches to use Value variants instead of Term
  variants (e.g. Value::Prim(...) instead of Term::Prim(...))
- Correct assertion for universe type: use Value::U(Phase) not Value::Prim
- Tests now work with the semantic domain directly, more faithful to actual
  implementation and cleaner architecture

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

- Simplify prototype_eval.md section 6: generalize literal type handling
  without mentioning specific type_of API
- Rewrite self_typed_ir.md: focus on semantic vs syntactic type design
  decision rather than implementation details that drift
- Simplify nbe_and_debruijn.md: replace detailed code samples with
  high-level descriptions of eval/apply/quote/type-checker integration
- Emphasize architectural principles over specific function signatures
  and parameter names, making docs more resilient to implementation changes

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

Emphasize focusing on concepts and design decisions rather than
implementation-specific details that can drift as code evolves.

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

…ated guide

Move implementation-specific sections (NbE, De Bruijn, references, glossary) from
kovacs-2022-staged-compilation-2ltt.md to implementation-guide.md. The Kovacs file
now contains only the paper extract, while implementation details belong in the
dedicated practical guide.

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

Keep pi_types.md listed only in Compiler Internals section with the more
complete description that captures both design decisions and implementation
details (NbE type checking).

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

… pretty.rs match

- Add Lvl::ix_at_depth(self, depth: Lvl) -> Ix and Ix::lvl_at_depth(self, depth: Lvl) -> Lvl
  methods to core/mod.rs for De Bruijn level<->index conversions
- Replace standalone lvl_to_ix/ix_to_lvl function calls with method calls in value.rs
  and checker/mod.rs
- Remove lvl_to_ix import from value.rs and checker/mod.rs since now using methods
- Simplify pretty.rs:fmt_term match: replace explicit enum arm list with wildcard (_)
  for all variants except Let and Match

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

All callers have been converted to use the Lvl::ix_at_depth() and Ix::lvl_at_depth()
methods instead. Remove the standalone function definitions to avoid duplication and
encourage use of the method-based API.

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

Replace manual De Bruijn index-to-level conversion (checked_sub pattern) with
the Ix::lvl_at_depth() method call.

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

Replace manual De Bruijn index-to-level conversion (checked_sub pattern) with
the Ix::lvl_at_depth() method call for consistency.

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

…Prim::U

Value::U(Phase) is redundant since Prim::U(Phase) already exists. All
match sites that handled Value::U(p) are updated to use
Value::Prim(Prim::U(p)) instead.

Updated:
- core/value.rs: quote function, apply function, value_phase function
- checker/mod.rs: val_type_of creation, type_phase, check_lift
- checker/test/meta.rs: test assertion

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

Replace the nonsensical placeholder Value::Rigid(Lvl(usize::MAX)) with
unreachable!() since this code path should never be reached in well-typed programs.

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

Empty slices don't need arena allocation; use the static empty slice &[]
directly for the args in stuck App values.

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

Add comment referencing GitHub issue #24 about the hardcoded u64 type
used when binding pattern-matched values. Type should come from
the scrutinee, not be hardcoded.

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

- Changed core::Pat::Bind from Bind(&str) to Bind(Name)
- Changed core::Let::name from &str to Name
- Changed core::Lam params from &[(& str, &Term)] to &[(Name, &Term)]
- Changed core::Pi params from &[(&str, &Term)] to &[(Name, &Term)]
- Updated Ctx.names from Vec<&core str> to Vec<core::Name>
- Updated Ctx method signatures (push_local, push_local_val, push_let_binding, lookup_local) to use Name
- Updated elaboration code to construct Name values at allocation time
- Updated test code push_local calls to wrap strings with core::Name::new()
- Work in progress: still fixing remaining callsites in pretty.rs, eval.rs, and test files

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

- Fixed all callsites where core IR structures are constructed or used
- Updated pretty.rs to use Name in environment instead of &str
- Updated value.rs VLam and VPi to store Name instead of &str
- Updated eval.rs unstaging code to construct Name when creating Let and Pat
- Updated all test files to wrap string literals with core::Name::new()
- Fixed clippy error in globals lookup

All tests pass (163 tests), clippy clean.

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

Split the ref_cast_custom constructor into a private new_unchecked and
a public new that asserts the name is non-empty.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>